s SATISFIABLE
v 0
